\begin{tabbing}
R{-}state{-}var($i$;${\it ds}$;${\it da}$;$x$;$T$;${\it ks}$;${\it tr}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\oplus$$k$$\in$${\it ks}$.@$i$ \=\+\+
\\[0ex]ef\=fect $k$(v:Valtype(${\it da}$;$k$))\+
\\[0ex]$x$ := $\lambda$$s$,$v$. ${\it tr}$($k$,$s$,$v$,$s$($x$)) State(fpf{-}join(IdDeq;${\it ds}$;$x$ : $T$)) v 
\-\-\\[0ex]$\oplus$ @$i$ only events in ${\it ks}$ change $x$:$T$
\-
\end{tabbing}